Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar1/D33SLASH11.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

Q is empty.

↳ QTRS

  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

Q DP problem:
The TRS P consists of the following rules:

D¹₁(*₂(x, y)) -> D¹₁(x)
D¹₁(minus₁(x)) -> D¹₁(x)
D¹₁(*₂(x, y)) -> D¹₁(y)
D¹₁(+₂(x, y)) -> D¹₁(x)
D¹₁(+₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(x)
D¹₁(ln₁(x)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(x)
D¹₁(-₂(x, y)) -> D¹₁(y)
D¹₁(-₂(x, y)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(y)

The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

D¹₁(*₂(x, y)) -> D¹₁(x)
D¹₁(minus₁(x)) -> D¹₁(x)
D¹₁(*₂(x, y)) -> D¹₁(y)
D¹₁(+₂(x, y)) -> D¹₁(x)
D¹₁(+₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(x)
D¹₁(ln₁(x)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(x)
D¹₁(-₂(x, y)) -> D¹₁(y)
D¹₁(-₂(x, y)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(y)

The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

D¹₁(*₂(x, y)) -> D¹₁(x)
D¹₁(*₂(x, y)) -> D¹₁(y)
D¹₁(+₂(x, y)) -> D¹₁(x)
D¹₁(+₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(y)
D¹₁(pow₂(x, y)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(x)
D¹₁(-₂(x, y)) -> D¹₁(y)
D¹₁(-₂(x, y)) -> D¹₁(x)
D¹₁(div₂(x, y)) -> D¹₁(y)

Used argument filtering: D¹₁(x1) = x1
*₂(x1, x2) = *₂(x1, x2)
minus₁(x1) = x1
+₂(x1, x2) = +₂(x1, x2)
pow₂(x1, x2) = pow₂(x1, x2)
ln₁(x1) = x1
div₂(x1, x2) = div₂(x1, x2)
-₂(x1, x2) = -₂(x1, x2)
Used ordering: Precedence:

trivial

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ QDPAfsSolverProof

            ↳ QDP

              ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

D¹₁(minus₁(x)) -> D¹₁(x)
D¹₁(ln₁(x)) -> D¹₁(x)

The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

D¹₁(ln₁(x)) -> D¹₁(x)

Used argument filtering: D¹₁(x1) = x1
minus₁(x1) = x1
ln₁(x1) = ln₁(x1)
Used ordering: Precedence:

trivial

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ QDPAfsSolverProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

D¹₁(minus₁(x)) -> D¹₁(x)

The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

D¹₁(minus₁(x)) -> D¹₁(x)

Used argument filtering: D¹₁(x1) = x1
minus₁(x1) = minus₁(x1)
Used ordering: Precedence:

trivial

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ QDPAfsSolverProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ QDPAfsSolverProof

                    ↳ QDP

                      ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

D₁(t) -> 1
D₁(constant) -> 0
D₁(+₂(x, y)) -> +₂(D₁(x), D₁(y))
D₁(*₂(x, y)) -> +₂(*₂(y, D₁(x)), *₂(x, D₁(y)))
D₁(-₂(x, y)) -> -₂(D₁(x), D₁(y))
D₁(minus₁(x)) -> minus₁(D₁(x))
D₁(div₂(x, y)) -> -₂(div₂(D₁(x), y), div₂(*₂(x, D₁(y)), pow₂(y, 2)))
D₁(ln₁(x)) -> div₂(D₁(x), x)
D₁(pow₂(x, y)) -> +₂(*₂(*₂(y, pow₂(x, -₂(y, 1))), D₁(x)), *₂(*₂(pow₂(x, y), ln₁(x)), D₁(y)))

The set Q consists of the following terms:

D₁(t)
D₁(constant)
D₁(+₂(x0, x1))
D₁(*₂(x0, x1))
D₁(-₂(x0, x1))
D₁(minus₁(x0))
D₁(div₂(x0, x1))
D₁(ln₁(x0))
D₁(pow₂(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.